Cyber-physical systems have tightly interacting physical and computational parts
Model system behavior as the passing around and processing of signals (e.g. real numbers).
Interaction can be thought of as variable sharing
Physical coupling between train cars forces their velocity to be the same
Categorical treatment of co-design problem allowed us to evaluate composite feasibility relation from a diagram of simpler feasibility relations.
Likewise we can evaluate whether two different signal flow graphs specify the same composite system
(perhaps to validate that a system meets a given specification)
Symmetric monoidal preorders were a special class of symmetric monoidal category where morphisms are constrained to be simple (at most one between any pair of objects).
Signal flow diagrams can be modeled by props, which is a special class of symmetricf monoidal category where objects are constrained to be simple (all are generaated by the monoidal product of a single object).
In the former we have to label wires but not boxes. Vice-versa for props.
Each object is the n-fold monoidal product of the generating object \(1\).
To specify a prop \(P\) it is enough to specify 5 things (and check they satisfy the rules for symmetric monoidal categories):
A set \(\mathcal{C}(m,n))\) of morphisms \(m \rightarrow n\) for \(m,n \in \mathbb{N}\).
For all naturals, an identity map \(n \xrightarrow{id_n} n\)
For all \(m,n \in \mathbb{N}\), a symmetry map \(m+n \xrightarrow{\sigma_{m,n}} n+m\)
A composition rule: given \(m \xrightarrow f n\) and \(n \xrightarrow g p\), a map \(m \xrightarrow{f;g} p\)
A monoidal product on morphisms: given \(m \xrightarrow f m'\) and \(n \xrightarrow g n'\), a map \(m+n \xrightarrow{f+g} m' +n'\)
A prop
A symmetric strict monoidal category \((\mathcal{C}, 0,+)\) for which \(Ob(\mathcal{C})=\mathbb{N}\) and the monoidal product on objects is given by addition.
A \(\ref{Prop|\emph{prop|referenced}}\) functor \(\mathcal{C} \xrightarrow F \mathcal{D}\) A functor for which
\(\forall n \in \mathbb{N}: F(n)=n\)
For all \(m_1 \xrightarrow f m_2\) and \(n_1 \xrightarrow g n_2 \in \mathcal{C}\): \(F(f))+F(g)=F(f+g) \in \mathcal{D}\)
The prop FinSet
Morphisms \(m \xrightarrow f n\) are functions from \(\bar m\) to \(\bar n\).
The identities, symmetries, and composition rule are obvious.
The monoidal product on functions is given by the disjoint union.
The compact closed category \(\ref{Correl as CCC|\textbf{Corel|referenced}}\) is a prop.
There is a prop Rel
Morphisms are relations \(R \subseteq \bar m \times \bar n\)
Composition with \(S \subseteq \bar n \times \bar p\) is
\(\{(i, k)\ |\ \exists (i, j) \in R \land \exists (j,k) \in S\}\)
Monoidal product is given by the coproduct, which amounts to placing the two relations side-by-side.
The inclusion \(\mathbf{Bij} \overset{i}{\hookrightarrow} \mathbf{FinSet}\) is a prop functor.
There is a prop functor \(\mathbf{Bij} \xrightarrow F \mathbf{Rel_{Fin}}\) defined by \(F(\bar{m} \xrightarrow{f} \bar{n}):=\{(i,j)\ |\ f(i)=j\} \in \bar m \times \bar n\)
Draw a morphism \(3 \xrightarrow f 2\) and a morphism \(2 \xrightarrow g 4\) in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\)
Draw \(f+g\)
What is the natural composition rule for morphisms in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\)
What are the identities in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\)
Draw a symmetry map \(\sigma_{m,n}\) for some \(m,n\) in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\).
TODO
A posetal prop is a prop that is also a poset.
In other words, a symmetric monoidal preorder \((\mathbb{N}, \leq)\) for some posetal relation \(\leq\), where the monoidal product is addition.
Give three examples of a posetal prop.
The normal meaning of \(\leq\) as less than or equal to
The divisibility relation
The opposite of the first example (greater than or equal to).
A port graph
A special type of prop where morphisms are open, directed, acyclic port graphs \((V, in, out, i)\)
\(V\) is a set of vertices
functions \(V \xrightarrow{in, out} \mathbb{N}\) give the in degree and out degree of each vertex
A bijection \(\bar m \sqcup O \xrightarrow{i} I \sqcup \bar n\), where \(I = \{(v,i)\ |\ v \in V, 1 \leq i \leq in(v)\}\) and \(O=\{(v,i)\ |\ v \in V, 1 \leq i \leq out(v))\}\) are the vertex inputs and vertex outputs, respectively.
Furthermore, an acyclicity condition:
Use the bijection \(i\) to construct the internal flow graph: a graph with an arrow \(u \xrightarrow{e^{u,i}_{v,j}} v\) for every \(i,j \in \mathbb{N}\) such that \(i(u,i)=(v,j)\)
This graph must be acyclic
A \((2,3)\) port-graph. [Draw this]
Since the overall type is \((2,3)\) we know we need a box with two overall inputs and three overall outputs.
There are three internal boxes, meaning the vertex set is \(\{a, b, c\}\).
\(in(a)=1\) and \(out(a)=3\) which tells us to draw one port on the LHS and three on the RHS.
The bijection \(i\) tells us how the ports are connected by wires.
The acyclic internal flow graph is shown below [TODO Draw this]
A category PG whose objects are natural numbers and morphisms are port graphs
We can compose a \((m,n)\) port graph with a \((n, p)\) port graph \((V \sqcup V',[in,in'],[out,out'], i'')\)
\(V \sqcup V' \xrightarrow{[in,in']} \mathbb{N}\) maps elements of \(V\) according to \(in\) and elements of \(V'\) according to \(in'\) (likewise for out).
The bijection \(\bar m \sqcup O \sqcup O' \xrightarrow{i''} I \sqcup I' \sqcup \bar p\) is defined as \(i''(x)=\begin{cases}i(x) & i(x) \in I \\ i'(i(x))& i(x) \in \bar n \\ i'(x) & x \in O' \end{cases}\)
The identity port graph on \(n\) is \((\varnothing, !, !, id_{\bar n})\) where \(\varnothing \xrightarrow{!} \mathbb{N}\) is a unique function.
This category is a prop.
The monoidal product of two portgraphs... TODO
Describe how port graph composition looks, with respect to the visual representation of Example 5.14, and give a nontrivial example
Todo